core_mmu.c (550): size_t n = 0;
core_mmu.c (551): paddr_t pa;
core_mmu.c (552): paddr_size_t size;
core_mmu.c (566): while (true) {  *** Loop condition evaluation: 1 (true)  *** Entering the loop
core_mmu.c (567): if (n >= (num_elems - 1)) {  *** Condition evaluation: (n >= num_elems - 1) (assuming false)
Point where number of bytes to process is defined
core_mmu.c (571): if (n == *last)  *** Buffer: tee_mmap_region memory_map + n + 1[]  *** Condition evaluation: (n == *last) (assuming true)
core_mmu.c (572): break;  *** Exit the loop
core_mmu.c (590): memmove(memory_map + n + 1, memory_map + n,
core_mmu.c (591): sizeof(struct tee_mmap_region) * (*last - n));
Point where buffer is passed to the function 
core_mmu.c (590): memmove(memory_map + n + 1, memory_map + n,  *** Number of bytes to process: 40 * *last - n == 0  *** Buffer: tee_mmap_region memory_map + n + 1[]

core_mmu.c (602): size_t n = 0;
core_mmu.c (605): while (true) {  *** Loop condition evaluation: 1 (true)  *** Entering the loop
core_mmu.c (606): if (n >= (num_elems - 1)) {  *** Condition evaluation: (n >= num_elems - 1) (assuming false)
Point where number of bytes to process is defined
core_mmu.c (610): if (n == *last)  *** Buffer: tee_mmap_region memory_map + n + 1[]  *** Condition evaluation: (n == *last) (assuming true)
core_mmu.c (611): break;  *** Exit the loop
core_mmu.c (617): memmove(memory_map + n + 1, memory_map + n,
core_mmu.c (618): sizeof(struct tee_mmap_region) * (*last - n));
Point where buffer is passed to the function 
core_mmu.c (617): memmove(memory_map + n + 1, memory_map + n,  *** Number of bytes to process: 40 * *last - n == 0  *** Buffer: tee_mmap_region memory_map + n + 1[]

Example path
        boot.c (1149): assert(phys_ddr_overall_compat_begin ==  *** Method call  *** Example of checking
Violation path
        Method call
        core_mmu.c (852): scattered_array_relax_ptr(...)
        core_mmu.c (852): phys_sdp_mem_begin,
        core_mmu.c (853): phys_sdp_mem_end, "SDP");
        Point by which returned value should be checked 
        core_mmu.c (851): verify_special_mem_areas(memory_map, num_elems,

Point where value is declared
Point where value is declared 
snprintk.c (270): size = 0; /* XXX: shutup gcc */

Start of the path
strlcat.c (66): while (*s != '\0') {  *** Loop condition evaluation: (int)*s != 0 (assuming true)  *** Entering the loop
strlcat.c (67): if (n != 1) {  *** Condition evaluation: (n != 1) (assuming false)
strlcat.c (71): s++;
strlcat.c (66): while (*s != '\0') {  *** Loop condition evaluation: (*s != 0) (true)  *** Entering the loop
strlcat.c (67): if (n != 1) {  *** Condition evaluation: n != 1 (assuming 1) -> n = 0  *** Condition evaluation: (n != 1) (assuming true)
strlcat.c (68): *d++ = *s;
Integer overflow point 
strlcat.c (69): n--;  *** Variable assignment: n = --n -> n = 18446744073709551615